es:ES, P:(E), R:(EE).
single-thread-generator{i:l}(es;P;R)
 (e, e':E. (R(e,e'))  (P(e) & P(e')))
 (e, a:E. P(e)  P(a)  (e < a)  (m:E. (P(m) & R(e,m) & (R^*)(m,a)))) 

latex

Definitions	{T}, x f y, P  Q, A c B, x:A. B(x), t  T, x(s), P & Q, P  Q, , x:A. B(x), P  Q, False, P  Q
Lemmas	rel-plus-rel-star, rel star iff, rel star wf, rel plus implies2, es-causl irreflexivity, es-causl transitivity2, es-le weakening eq, es-le-causle, es-causle weakening, event system wf, single-thread-generator wf, es-E wf, es-causl wf, generated-thread-properties2